(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_IDL)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(assert (let ((e2 6))
(let ((e3 0))
(let ((e4 0))
(let ((e5 1))
(let ((e6 4))
(let ((e7 (> v0 v1)))
(let ((e8 (distinct (- v1 v0) e6)))
(let ((e9 (< v1 v0)))
(let ((e10 (>= (- v1 v1) (- e4))))
(let ((e11 (= v1 v0)))
(let ((e12 (>= (- v0 v0) e4)))
(let ((e13 (< v1 v0)))
(let ((e14 (distinct (- v0 v0) e5)))
(let ((e15 (<= v0 v1)))
(let ((e16 (<= (- v0 v0) (- e4))))
(let ((e17 (>= (- v1 v0) e2)))
(let ((e18 (> (- v0 v0) e4)))
(let ((e19 (>= (- v0 v1) e6)))
(let ((e20 (= v0 v1)))
(let ((e21 (> (- v1 v0) (- e3))))
(let ((e22 (= (- v1 v0) (- e2))))
(let ((e23 (<= (- v1 v1) e6)))
(let ((e24 (distinct v0 v0)))
(let ((e25 (< (- v0 v0) e6)))
(let ((e26 (< (- v1 v0) (- e6))))
(let ((e27 (<= v1 v1)))
(let ((e28 (<= v0 v0)))
(let ((e29 (> v1 v0)))
(let ((e30 (> (- v0 v0) e6)))
(let ((e31 (>= v0 v0)))
(let ((e32 (< v0 v1)))
(let ((e33 (= v0 v0)))
(let ((e34 (<= (- v0 v1) e5)))
(let ((e35 (distinct (- v1 v0) (- e5))))
(let ((e36 (= v1 v1)))
(let ((e37 (< v0 v0)))
(let ((e38 (< v0 v0)))
(let ((e39 (distinct (- v0 v0) (- e4))))
(let ((e40 (= (- v0 v1) e2)))
(let ((e41 (> v1 v0)))
(let ((e42 (> v0 v0)))
(let ((e43 (> (- v0 v0) e5)))
(let ((e44 (distinct (- v1 v1) e5)))
(let ((e45 (distinct v0 v1)))
(let ((e46 (distinct (- v1 v0) e4)))
(let ((e47 (distinct v0 v1)))
(let ((e48 (> v1 v1)))
(let ((e49 (distinct v0 v1)))
(let ((e50 (distinct (- v0 v0) (- e5))))
(let ((e51 (= (- v1 v0) e4)))
(let ((e52 (>= v0 v1)))
(let ((e53 (> v1 v0)))
(let ((e54 (>= v0 v1)))
(let ((e55 (>= (- v1 v1) (- e3))))
(let ((e56 (< v0 v0)))
(let ((e57 (> v1 v0)))
(let ((e58 (= (- v0 v0) e5)))
(let ((e59 (<= v1 v1)))
(let ((e60 (distinct (- v0 v1) (- e4))))
(let ((e61 (>= (- v0 v0) e3)))
(let ((e62 (=> e46 e57)))
(let ((e63 (not e22)))
(let ((e64 (and e37 e16)))
(let ((e65 (or e48 e13)))
(let ((e66 (not e39)))
(let ((e67 (or e60 e52)))
(let ((e68 (and e36 e21)))
(let ((e69 (and e25 e33)))
(let ((e70 (= e58 e9)))
(let ((e71 (not e8)))
(let ((e72 (xor e26 e7)))
(let ((e73 (xor e63 e51)))
(let ((e74 (=> e61 e28)))
(let ((e75 (ite e11 e20 e41)))
(let ((e76 (and e31 e19)))
(let ((e77 (xor e15 e71)))
(let ((e78 (or e49 e76)))
(let ((e79 (ite e54 e55 e24)))
(let ((e80 (=> e34 e47)))
(let ((e81 (=> e38 e75)))
(let ((e82 (xor e30 e77)))
(let ((e83 (=> e23 e78)))
(let ((e84 (and e27 e69)))
(let ((e85 (or e17 e12)))
(let ((e86 (ite e29 e62 e83)))
(let ((e87 (or e14 e80)))
(let ((e88 (= e86 e32)))
(let ((e89 (= e85 e81)))
(let ((e90 (or e40 e45)))
(let ((e91 (= e79 e68)))
(let ((e92 (or e90 e35)))
(let ((e93 (ite e70 e53 e44)))
(let ((e94 (not e87)))
(let ((e95 (=> e59 e94)))
(let ((e96 (not e43)))
(let ((e97 (ite e95 e42 e74)))
(let ((e98 (= e73 e84)))
(let ((e99 (or e82 e93)))
(let ((e100 (not e67)))
(let ((e101 (not e100)))
(let ((e102 (not e88)))
(let ((e103 (=> e64 e96)))
(let ((e104 (or e89 e50)))
(let ((e105 (or e18 e98)))
(let ((e106 (=> e103 e104)))
(let ((e107 (ite e106 e99 e102)))
(let ((e108 (xor e91 e66)))
(let ((e109 (=> e65 e10)))
(let ((e110 (xor e101 e105)))
(let ((e111 (xor e108 e72)))
(let ((e112 (=> e111 e97)))
(let ((e113 (and e92 e110)))
(let ((e114 (= e107 e109)))
(let ((e115 (and e114 e114)))
(let ((e116 (not e56)))
(let ((e117 (xor e116 e115)))
(let ((e118 (not e113)))
(let ((e119 (or e112 e118)))
(let ((e120 (and e119 e117)))
e120
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
